package tr.edu.ege.kipler.syntax.atomicformula;

import tr.edu.ege.kipler.syntax.BinaryBooleanExpression;
import tr.edu.ege.kipler.syntax.ModalExpression;
import tr.edu.ege.kipler.syntax.WorldElementVisitor;

/**
 * Calculates the modal depth of a formula which means the maximal depth of
 * nested modal operators in that formula.
 * 
 * @author İnanç Seylan
 * 
 */
public class ModalDepthVisitor implements WorldElementVisitor {
	/**
	 * This field stores the modal depth of a given formula and is modified by
	 * all the methods in this class.
	 */
	private int depth;

	/**
	 * @return the calculated modal depth.
	 */
	public int getDepth() {
		return depth;
	}

	/**
	 * Increments the value of {@link #depth} and constructs a new
	 * {@link ModalDepthVisitor} to visit the necessiate/possibilitate. Then
	 * adds the value returned by that visitor to {@link #depth}.
	 * 
	 * @see tr.edu.ege.seagent.alcbi.syntax.FormulaVisitor#visitModalFormula(tr.edu.ege.seagent.alcbi.syntax.ModalFormula)
	 */
	public void visitModalElement(ModalExpression mf) {
		depth++;
		ModalDepthVisitor mdv = new ModalDepthVisitor();
		mf.getExpression().accept(mdv);
		depth += mdv.getDepth();
	}

	/**
	 * Constructs a new {@link ModalDepthVisitor} once for the left operand and
	 * once for the right operand. Then adds the greatest modal depth of the two
	 * visitors to {@link #depth}.
	 * 
	 * @see tr.edu.ege.seagent.alcbi.syntax.FormulaVisitor#visitBinaryBooleanFormula(tr.edu.ege.seagent.alcbi.syntax.BinaryBooleanFormula)
	 */
	public void visitBinaryElement(BinaryBooleanExpression bf) {
		ModalDepthVisitor mdv = new ModalDepthVisitor();
		bf.getLhs().accept(mdv);
		int leftDepth = mdv.getDepth();
		mdv = new ModalDepthVisitor();
		bf.getRhs().accept(mdv);
		int rightDepth = mdv.getDepth();
		if (leftDepth > rightDepth)
			depth += leftDepth;
		else
			depth += rightDepth;
	}

	public void visitConceptAssertion(ConceptAssertion ca) {
		// nothing to do

	}

	public void visitConceptDefinition(ConceptDefinition cd) {
		// nothing to do
	}

	public void visitObjectRoleAssertion(ObjectRoleAssertion ra) {
		// nothing to do
	}

	public void visitRoleAssertion(RoleAssertion ra) {
		// nothing to do
	}

	public void visitRoleInclusion(RoleInclusion ri) {
		// nothing to do
	}

	public void visitSameIndividualAssertion(SameIndividualAssertion ia) {
		// nothing to do
	}

}
